$\forall$$M$:MsgA, $s$:$M$.(timed)state. shift{-}state($s$) $\in$ $M$.(timed)state